Struct isotope::term::Case [−][src]
pub struct Case { /* fields omitted */ }
Expand description
A case expression, which switches on variants to return a value
Implementations
pub fn new_unchecked(
cases: Arc<[TermId]>,
matches: TermId,
annot: Option<Annotation>
) -> Case
[src]
pub fn new_unchecked(
cases: Arc<[TermId]>,
matches: TermId,
annot: Option<Annotation>
) -> Case
[src]Construct a new case expression without performing any checks
Construct a new case expression with the minium possible type
Compute the form of a case statement
Compute the code of a case statement
pub fn compute_filter(
cases: &[TermId],
matches: &TermId,
annot: Option<&Annotation>
) -> VarFilter
[src]
pub fn compute_filter(
cases: &[TermId],
matches: &TermId,
annot: Option<&Annotation>
) -> VarFilter
[src]Compute the filter of a case statement
pub fn compute_flags(
_cases: &[TermId],
_matches: &TermId,
_annot: Option<&Annotation>
) -> TyckFlags
[src]
pub fn compute_flags(
_cases: &[TermId],
_matches: &TermId,
_annot: Option<&Annotation>
) -> TyckFlags
[src]Compute the flags of a case statement
Compute the minimal type of a case expression
Compute the minimal parameter type of a case expression
Compute the minimal result type of a case expression
Count the number of cases to match, given a set of matches, as well as whether fallback is possible
Create a match for the ix
th case
Get the index an argument matches, if any
Trait Implementations
Cons this term within a given context. Return None
if already consed.
Convert this term to it’s own consed type
Whether this term depends on a variable with a given index: if equiv is true, also consider larger variables in the same equivalence class
Get whether a term depends on a variable base <= variable <= ix
Read more
Get the variable filter of this term
type Substituted = Case
type Substituted = Case
The type this substitutes to
Substitute this value recursively
Convert this object’s consed form to it’s substituted form
Shift this term’s variables with index >= base
in a given context
Shift this term’s variables with index >= base
in a given context
Locally typecheck a term: note this is context-independent, without caching
Globally typecheck a term, i.e. typecheck all subterms, without caching
Typecheck this term’s annotation, without caching
Load this term’s current flags
Set this term’s flags. May cause errors if done incorrectly!
Locally typecheck a term: note this is context-independent.
Globally typecheck a term, i.e. typecheck all subterms and their variables
Variable typecheck a term, i.e. typecheck all subterms and their variables.
Typecheck this term’s annotation
Globally typecheck a term and it’s annotation, i.e. typecheck all subterms, annotation subterms, and their variables
Typecheck a term in a given context
Typecheck this term along with it’s variables
Whether this term might be type-checked
type ValueConsed = Case
type ValueConsed = Case
The type of value this is consed to
type ValueSubstituted = Case
type ValueSubstituted = Case
The type of value this is substituted to
Convert this term to a Term
, without any consing
Get the type annotation of this term
Get whether this term is a type
Get whether this term is a universe
Get whether this term is a function
Get whether this term is a dependent function type
fn annotate_unchecked(
&self,
annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Self::ValueConsed>, Error>
[src]
fn annotate_unchecked(
&self,
annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Self::ValueConsed>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in a given context
Get the hash-code of this term if it was untyped Read more
Compare this term to another within a given context
Coerce this term to another type, with type-checking
Apply this value, as a function, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Get the index of this term in a program graph. Return None
if this term is unindexed
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in general
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]Cast this type into another in a given typing context
Substitute this term’s variables recursively given a context
Substitute this term’s variables given a context
Shift this term’s variables with index >= base
up by n
in a given context
Shift this term’s variables with index >= base
up by n
in a given context
Compare this term to a term ID, within a given context
Cons this term within a given context. Return None
if already consed.
Convert this term to a TermId
within a given context
Get the type of this term, if any
Get the type of this term, if any
Apply this value, as a dependent function type, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Convert this term to a TermId
, without any consing
Clone this term to a TermId
, without any consing
Clone this term to a TermId
within a given context
Clone this term to a Term
without any consing
Shallow cons a term directly into a context
Shallow cons a term directly into a context, cloning if necessary
Convert this term to a normal form
Convert this term a normal form
Convert this term to a normal form, or reduce it up to n
steps
Convert this term a normal form, or reduce it up to n
steps
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to a normal form, or reduce it up to n
steps
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]Convert this term a normal form, or reduce it up to n
steps
Auto Trait Implementations
impl !RefUnwindSafe for Case
impl !UnwindSafe for Case
Blanket Implementations
Mutably borrows from an owned value. Read more
Borrow an optional value of type T
Cons this term within a given context. Return None
if already consed.
Get the type annotation of this term
Get the index of this term in an isotope
program graph, if any
Get whether this term is a type
Get whether this term is a universe
Get whether this term is in “root form”
Get whether this term is a subtype of another term in a given context
Get whether this term has a universe in all contexts
Get the untyped hash-code of this term
Get the variable filter of this term
Shift this term’s variables with index >= base
up by n
in a given context
Whether this term has a given variable dependency
Whether this term has a given variable dependency below ix
and above base
Load this term’s flags
Set this term’s flags
Compare this term to another dynamic term
Compare this term to another
Compare this term to a term ID
Compare self to key
and return true
if they are equal.